Dependently typed lambda calculi such as the Logical Framework (LF) canencode relationships between terms in types and can naturally capturecorrespondences between formulas and their proofs. Such calculi can also begiven a logic programming interpretation: the Twelf system is based on such aninterpretation of LF. We consider here whether a conventional logic programminglanguage can provide the benefits of a Twelf-like system for encoding type andproof-and-formula dependencies. In particular, we present a simple mapping fromLF specifications to a set of formulas in the higher-order hereditary Harrop(hohh) language, that relates derivations and proof-search between the twoframeworks. We then show that this encoding can be improved by exploitingknowledge of the well-formedness of the original LF specifications to elidemuch redundant type-checking information. The resulting logic program has astructure that closely resembles the original specification, thereby allowingLF specifications to be viewed as hohh meta-programs. Using the Teyjusimplementation of lambdaProlog, we show that our translation provides anefficient means for executing LF specifications, complementing the ability thatthe Twelf system provides for reasoning about them.
展开▼
